$\forall$$A$:Type, ${\it as}$:$A$ List. ${\it as}$ $=$ nil $\Rightarrow$ $\parallel$${\it as}$$\parallel$ $=$ 0